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