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