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