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