Anne is quiet. Anne is smart. Anne is young. Bob is furry. Bob is green. Charlie is nice. Fiona is furry. Fiona is green. Fiona is rough. Fiona is smart. Fiona is young. If something is green and rough then it is smart. If something is nice and not green then it is young. If something is smart and rough then it is young. If something is nice then it is not furry. If Anne is green and Anne is young then Anne is not nice. All young, green things are not nice. All green things are rough. If Bob is not nice then Bob is not quiet. If Anne is young and Anne is not nice then Anne is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is green and rough then it is smart.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is nice and not green then it is young.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "+"))
If something is smart and rough then it is young.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is not furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "-"))
If Anne is green and Anne is young then Anne is not nice.
((("Anne" "is" "green" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "nice" "-"))
All young, green things are not nice.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "-"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If Bob is not nice then Bob is not quiet.
((("Bob" "is" "nice" "~")) -> ("Bob" "is" "quiet" "-"))
If Anne is young and Anne is not nice then Anne is quiet.
((("Anne" "is" "young" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "quiet" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Bob is not green.
False
1
inv-proof
[(triple5)]
("Bob" "is" "green" "-")
triple5
Bob is rough.
True
2
proof
[(((triple5) -> rule7))]
("Bob" "is" "rough" "+")
((triple5) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple5) -> rule7))]
("Bob" "is" "rough" "-")
((triple5) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
True
4
proof
[(((triple5 ((triple5) -> rule7)) -> rule1))]
("Bob" "is" "smart" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((triple5 ((triple5) -> rule7)) -> rule1))]
("Bob" "is" "smart" "-")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is young.
True
7
proof
[(((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3))]
("Bob" "is" "young" "+")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule1 % int2)) ((triple5) -> (rule7 % int3))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not young.
False
7
inv-proof
[(((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3))]
("Bob" "is" "young" "-")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule1 % int2)) ((triple5) -> (rule7 % int3))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not nice.
True
9
proof
[(((((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3) triple5) -> rule6))]
("Bob" "is" "nice" "-")
((((((triple5 ((triple5) -> (rule7 % int4))) -> (rule1 % int3)) ((triple5) -> (rule7 % int4))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is nice.
False
9
inv-proof
[(((((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3) triple5) -> rule6))]
("Bob" "is" "nice" "+")
((((((triple5 ((triple5) -> (rule7 % int4))) -> (rule1 % int3)) ((triple5) -> (rule7 % int4))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is not quiet.
True
10
proof
[(((((((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3) triple5) -> rule6)) -> rule8))]
("Bob" "is" "quiet" "-")
((((((((triple5 ((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((triple5) -> (rule7 % int5))) -> (rule3 % int3)) triple5) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
int5
Bob is quiet.
False
10
inv-proof
[(((((((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3) triple5) -> rule6)) -> rule8))]
("Bob" "is" "quiet" "+")
((((((((triple5 ((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((triple5) -> (rule7 % int5))) -> (rule3 % int3)) triple5) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
int5
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "rough" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Anne is smart.[(triple2)] Anne is young.[(triple3)] Bob is furry.[(triple4)] Bob is green.[(triple5)] Charlie is nice.[(triple6)] Fiona is furry.[(triple7)] Fiona is green.[(triple8)] Fiona is rough.[(triple9 OR ((triple8) -> rule7))] Fiona is smart.[(triple10 OR ((triple8 triple9) -> rule1) OR ((triple8 ((triple8) -> rule7)) -> rule1))] Fiona is young.[(triple11 OR ((triple10 triple9) -> rule3) OR ((triple10 ((triple8) -> rule7)) -> rule3) OR ((((triple8 triple9) -> rule1) triple9) -> rule3) OR ((((triple8 triple9) -> rule1) ((triple8) -> rule7)) -> rule3) OR ((((triple8 ((triple8) -> rule7)) -> rule1) triple9) -> rule3) OR ((((triple8 ((triple8) -> rule7)) -> rule1) ((triple8) -> rule7)) -> rule3))] @1: Bob is rough.[(((triple5) -> rule7))] Charlie is not furry.[(((triple6) -> rule4))] Fiona is not nice.[(((triple11 triple8) -> rule6) OR ((((triple10 triple9) -> rule3) triple8) -> rule6) OR ((((triple10 ((triple8) -> rule7)) -> rule3) triple8) -> rule6) OR ((((((triple8 triple9) -> rule1) triple9) -> rule3) triple8) -> rule6) OR ((((((triple8 triple9) -> rule1) ((triple8) -> rule7)) -> rule3) triple8) -> rule6) OR ((((((triple8 ((triple8) -> rule7)) -> rule1) triple9) -> rule3) triple8) -> rule6) OR ((((((triple8 ((triple8) -> rule7)) -> rule1) ((triple8) -> rule7)) -> rule3) triple8) -> rule6))] @2: Bob is smart.[(((triple5 ((triple5) -> rule7)) -> rule1))] @3: Bob is young.[(((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3))] @4: Bob is not nice.[(((((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3) triple5) -> rule6))] @5: Bob is not quiet.[(((((((((triple5 ((triple5) -> rule7)) -> rule1) ((triple5) -> rule7)) -> rule3) triple5) -> rule6)) -> rule8))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
((triple8) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple8 triple9) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 ((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple11
((triple10 triple9) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple10 ((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple8 triple9) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 triple9) -> (rule1 % int3)) ((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((triple8 ((triple8) -> (rule7 % int3))) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((triple8 ((triple8) -> (rule7 % int3))) -> (rule1 % int2)) ((triple8) -> (rule7 % int3))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((triple5) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple6) -> (rule4 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Fiona is not nice.
("Fiona" "is" "nice" "-")
((triple11 triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
((((triple10 triple9) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple10 ((triple8) -> (rule7 % int3))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((((triple8 triple9) -> (rule1 % int3)) triple9) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((triple8 triple9) -> (rule1 % int4)) ((triple8) -> (rule7 % int3))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((((triple8 ((triple8) -> (rule7 % int4))) -> (rule1 % int3)) triple9) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((((((triple8 ((triple8) -> (rule7 % int4))) -> (rule1 % int3)) ((triple8) -> (rule7 % int4))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule1 % int2)) ((triple5) -> (rule7 % int3))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not nice.
("Bob" "is" "nice" "-")
((((((triple5 ((triple5) -> (rule7 % int4))) -> (rule1 % int3)) ((triple5) -> (rule7 % int4))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is not quiet.
("Bob" "is" "quiet" "-")
((((((((triple5 ((triple5) -> (rule7 % int5))) -> (rule1 % int4)) ((triple5) -> (rule7 % int5))) -> (rule3 % int3)) triple5) -> (rule6 % int2))) -> (rule8 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
int5