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