Anne is blue. Anne is nice. Anne is red. Anne is round. Anne is white. Dave is big. Dave is blue. Dave is nice. Dave is red. Dave is white. Fiona is nice. Fiona is smart. Harry is blue. Harry is red. Harry is smart. If someone is big then they are round. Nice people are red. Big people are round. All big, smart people are blue. All red people are blue. All white, big people are round. If Anne is nice and Anne is round then Anne is blue. If Dave is big and Dave is white then Dave is round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All big, smart people are blue.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All white, big people are round.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Anne is nice and Anne is round then Anne is blue.
((("Anne" "is" "nice" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "blue" "+"))
If Dave is big and Dave is white then Dave is round.
((("Dave" "is" "big" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "round" "+"))
Dave is blue.
True
1
proof
[(triple7 OR ((triple9) -> rule5) OR ((((triple8) -> rule2)) -> rule5))]
("Dave" "is" "blue" "+")
triple7
((triple9) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is not nice.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "nice" "-")
triple11
Dave is round.
True
2
proof
[(((triple6) -> rule1) OR ((triple6) -> rule3) OR ((triple10 triple6) -> rule6) OR ((triple6 triple10) -> rule8))]
("Dave" "is" "round" "+")
((triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple10 triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6 triple10) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple6) -> rule1) OR ((triple6) -> rule3) OR ((triple10 triple6) -> rule6) OR ((triple6 triple10) -> rule8))]
("Dave" "is" "round" "-")
((triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple10 triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6 triple10) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple11) -> rule2)) -> rule5))]
("Fiona" "is" "blue" "+")
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule5))]
("Fiona" "is" "blue" "-")
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is blue.[(triple1 OR ((triple3) -> rule5) OR ((triple2 triple4) -> rule7) OR ((((triple2) -> rule2)) -> rule5))] Anne is nice.[(triple2)] Anne is red.[(triple3 OR ((triple2) -> rule2))] Anne is round.[(triple4)] Anne is white.[(triple5)] Dave is big.[(triple6)] Dave is blue.[(triple7 OR ((triple9) -> rule5) OR ((((triple8) -> rule2)) -> rule5))] Dave is nice.[(triple8)] Dave is red.[(triple9 OR ((triple8) -> rule2))] Dave is white.[(triple10)] Fiona is nice.[(triple11)] Fiona is smart.[(triple12)] Harry is blue.[(triple13 OR ((triple14) -> rule5))] Harry is red.[(triple14)] Harry is smart.[(triple15)] @1: Dave is round.[(((triple6) -> rule1) OR ((triple6) -> rule3) OR ((triple10 triple6) -> rule6) OR ((triple6 triple10) -> rule8))] Fiona is red.[(((triple11) -> rule2))] @2: Fiona is blue.[(((((triple11) -> rule2)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple3) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple2 triple4) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple9) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple8) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
((triple14) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple10 triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6 triple10) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple11) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple11) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2