Dave is green. Dave is red. Dave is rough. Dave is smart. Harry is big. Harry is blue. Harry is green. If someone is blue then they are smart. Smart, big people are cold.
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Smart, big people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Harry is green.
True
1
proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Harry is smart.
True
2
proof
[(((triple6) -> rule1))]
("Harry" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple6) -> rule1))]
("Harry" "is" "smart" "-")
((triple6) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
True
4
proof
[(((((triple6) -> rule1) triple5) -> rule2))]
("Harry" "is" "cold" "+")
((((triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((((triple6) -> rule1) triple5) -> rule2))]
("Harry" "is" "cold" "-")
((((triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is green.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3)] Dave is smart.[(triple4)] Harry is big.[(triple5)] Harry is blue.[(triple6)] Harry is green.[(triple7)] @1: Harry is smart.[(((triple6) -> rule1))] @2: Harry is cold.[(((((triple6) -> rule1) triple5) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is smart.
("Harry" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2