Dave is cold. Dave is rough. Erin is rough. Gary is cold. Gary is round. Harry is red. Harry is round. If Dave is cold then Dave is red. If someone is cold then they are blue. All red, blue people are big. Blue people are big. Cold people are rough. All round people are blue.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Dave is cold then Dave is red.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "red" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All red, blue people are big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Harry is red.
True
1
proof
[(triple6)]
("Harry" "is" "red" "+")
triple6
Erin is not rough.
False
1
inv-proof
[(triple3)]
("Erin" "is" "rough" "-")
triple3
Harry is blue.
True
2
proof
[(((triple7) -> rule6))]
("Harry" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule5))]
("Gary" "is" "rough" "-")
((triple4) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
True
3
proof
[(((((triple4) -> rule2)) -> rule4) OR ((((triple5) -> rule6)) -> rule4))]
("Gary" "is" "big" "+")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule4) OR ((((triple5) -> rule6)) -> rule4))]
("Gary" "is" "big" "-")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Dave is cold.[(triple1)] Dave is rough.[(triple2 OR ((triple1) -> rule5))] Erin is rough.[(triple3)] Gary is cold.[(triple4)] Gary is round.[(triple5)] Harry is red.[(triple6)] Harry is round.[(triple7)] @1: Dave is blue.[(((triple1) -> rule2))] Dave is red.[(((triple1) -> rule1))] Gary is blue.[(((triple4) -> rule2) OR ((triple5) -> rule6))] Gary is rough.[(((triple4) -> rule5))] Harry is blue.[(((triple7) -> rule6))] @2: Dave is big.[(((((triple1) -> rule2)) -> rule4) OR ((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3))] Gary is big.[(((((triple4) -> rule2)) -> rule4) OR ((((triple5) -> rule6)) -> rule4))] Harry is big.[(((((triple7) -> rule6)) -> rule4) OR ((triple6 ((triple7) -> rule6)) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
((triple1) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple5) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple6 ((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2