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