Erin is cold. Erin is round. Erin is white. Gary is white. Harry is cold. Harry is kind. Harry is white. All blue, round things are rough. All cold things are round. If something is white and round then it is blue.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
All blue, round things are rough.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is white and round then it is blue.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Harry is white.
True
1
proof
[(triple7)]
("Harry" "is" "white" "+")
triple7
Harry is not kind.
False
1
inv-proof
[(triple6)]
("Harry" "is" "kind" "-")
triple6
Harry is round.
True
2
proof
[(((triple5) -> rule2))]
("Harry" "is" "round" "+")
((triple5) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple5) -> rule2))]
("Harry" "is" "round" "-")
((triple5) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is rough.
True
5
proof
[(((((triple3 triple2) -> rule3) triple2) -> rule1) OR ((((triple3 triple2) -> rule3) ((triple1) -> rule2)) -> rule1) OR ((((triple3 ((triple1) -> rule2)) -> rule3) triple2) -> rule1) OR ((((triple3 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
("Erin" "is" "rough" "+")
((((triple3 triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple3 triple2) -> (rule3 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Harry is not blue.
False
4
inv-proof
[(((triple7 ((triple5) -> rule2)) -> rule3))]
("Harry" "is" "blue" "-")
((triple7 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
True
7
proof
[(((((triple7 ((triple5) -> rule2)) -> rule3) ((triple5) -> rule2)) -> rule1))]
("Harry" "is" "rough" "+")
((((triple7 ((triple5) -> (rule2 % int3))) -> (rule3 % int2)) ((triple5) -> (rule2 % int3))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not rough.
False
7
inv-proof
[(((((triple7 ((triple5) -> rule2)) -> rule3) ((triple5) -> rule2)) -> rule1))]
("Harry" "is" "rough" "-")
((((triple7 ((triple5) -> (rule2 % int3))) -> (rule3 % int2)) ((triple5) -> (rule2 % int3))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is cold.[(triple1)] Erin is round.[(triple2 OR ((triple1) -> rule2))] Erin is white.[(triple3)] Gary is white.[(triple4)] Harry is cold.[(triple5)] Harry is kind.[(triple6)] Harry is white.[(triple7)] @1: Erin is blue.[(((triple3 triple2) -> rule3) OR ((triple3 ((triple1) -> rule2)) -> rule3))] Harry is round.[(((triple5) -> rule2))] @2: Erin is rough.[(((((triple3 triple2) -> rule3) triple2) -> rule1) OR ((((triple3 triple2) -> rule3) ((triple1) -> rule2)) -> rule1) OR ((((triple3 ((triple1) -> rule2)) -> rule3) triple2) -> rule1) OR ((((triple3 ((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))] Harry is blue.[(((triple7 ((triple5) -> rule2)) -> rule3))] @3: Harry is rough.[(((((triple7 ((triple5) -> rule2)) -> rule3) ((triple5) -> rule2)) -> rule1))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
((triple3 triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple5) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3 triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple3 triple2) -> (rule3 % int3)) ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple3 ((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((triple7 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7 ((triple5) -> (rule2 % int3))) -> (rule3 % int2)) ((triple5) -> (rule2 % int3))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3