Anne is big. Anne is furry. Anne is green. Anne is nice. Anne is quiet. Anne is white. Anne is young. Bob is green. Fiona is big. Fiona is green. Fiona is nice. Fiona is white. If Anne is big and Anne is nice then Anne is furry. If something is white then it is nice. If Fiona is young then Fiona is nice. If Fiona is quiet and Fiona is green then Fiona is white. If Bob is big then Bob is nice. Green, young things are big. If something is nice and young then it is furry. All green things are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Anne is big and Anne is nice then Anne is furry.
((("Anne" "is" "big" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If Fiona is young then Fiona is nice.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "nice" "+"))
If Fiona is quiet and Fiona is green then Fiona is white.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "white" "+"))
If Bob is big then Bob is nice.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "nice" "+"))
Green, young things are big.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is nice and young then it is furry.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Fiona is big.
True
1
proof
[(triple9 OR ((triple10 ((triple10) -> rule8)) -> rule6))]
("Fiona" "is" "big" "+")
triple9
((triple10 ((triple10) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not green.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "green" "-")
triple10
Bob is young.
True
2
proof
[(((triple8) -> rule8))]
("Bob" "is" "young" "+")
((triple8) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple8) -> rule8))]
("Bob" "is" "young" "-")
((triple8) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is big.[(triple1 OR ((triple3 triple7) -> rule6) OR ((triple3 ((triple3) -> rule8)) -> rule6))] Anne is furry.[(triple2 OR ((triple1 triple4) -> rule1) OR ((triple4 triple7) -> rule7) OR ((triple1 ((triple6) -> rule2)) -> rule1) OR ((triple4 ((triple3) -> rule8)) -> rule7) OR ((((triple6) -> rule2) triple7) -> rule7) OR ((((triple3 triple7) -> rule6) triple4) -> rule1) OR ((((triple6) -> rule2) ((triple3) -> rule8)) -> rule7) OR ((((triple3 triple7) -> rule6) ((triple6) -> rule2)) -> rule1) OR ((((triple3 ((triple3) -> rule8)) -> rule6) triple4) -> rule1) OR ((((triple3 ((triple3) -> rule8)) -> rule6) ((triple6) -> rule2)) -> rule1))] Anne is green.[(triple3)] Anne is nice.[(triple4 OR ((triple6) -> rule2))] Anne is quiet.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7 OR ((triple3) -> rule8))] Bob is green.[(triple8)] Fiona is big.[(triple9 OR ((triple10 ((triple10) -> rule8)) -> rule6))] Fiona is green.[(triple10)] Fiona is nice.[(triple11 OR ((triple12) -> rule2) OR ((((triple10) -> rule8)) -> rule3))] Fiona is white.[(triple12)] @1: Bob is young.[(((triple8) -> rule8))] Fiona is young.[(((triple10) -> rule8))] @2: Bob is big.[(((triple8 ((triple8) -> rule8)) -> rule6))] Fiona is furry.[(((triple11 ((triple10) -> rule8)) -> rule7) OR ((((triple12) -> rule2) ((triple10) -> rule8)) -> rule7) OR ((((((triple10) -> rule8)) -> rule3) ((triple10) -> rule8)) -> rule7))] @3: Bob is nice.[(((((triple8 ((triple8) -> rule8)) -> rule6)) -> rule5))] @4: Bob is furry.[(((((((triple8 ((triple8) -> rule8)) -> rule6)) -> rule5) ((triple8) -> rule8)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3 triple7) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple3 ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple1 triple4) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 triple7) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple1 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple4 ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple6) -> (rule2 % int2)) triple7) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple3 triple7) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple3 triple7) -> (rule6 % int3)) ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((triple3 ((triple3) -> (rule8 % int3))) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple3 ((triple3) -> (rule8 % int4))) -> (rule6 % int3)) ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple6) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple3) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple8
Fiona is big.
("Fiona" "is" "big" "+")
triple9
((triple10 ((triple10) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
((triple12) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple10) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Bob is young.
("Bob" "is" "young" "+")
((triple8) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple10) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple8 ((triple8) -> (rule8 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple11 ((triple10) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple12) -> (rule2 % int3)) ((triple10) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((((triple10) -> (rule8 % int3))) -> (rule3 % int2)) ((triple10) -> (rule8 % int3))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((triple8 ((triple8) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple8 ((triple8) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple8) -> (rule8 % int4))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4