Bob is big. Bob is furry. Bob is nice. Dave is furry. Dave is red. Harry is big. Harry is furry. Harry is nice. Harry is red. Harry is smart. If Bob is red then Bob is smart. All furry, big people are smart. Cold people are big. Furry, big people are nice. Furry people are cold. Rough people are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Bob is red then Bob is smart.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "smart" "+"))
All furry, big people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Furry, big people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Harry is smart.
True
1
proof
[(triple10 OR ((triple7 triple6) -> rule2) OR ((triple7 ((((triple7) -> rule5)) -> rule3)) -> rule2))]
("Harry" "is" "smart" "+")
triple10
((triple7 triple6) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not nice.
False
1
inv-proof
[(triple8 OR ((triple7 triple6) -> rule4) OR ((triple7 ((((triple7) -> rule5)) -> rule3)) -> rule4))]
("Harry" "is" "nice" "-")
triple8
((triple7 triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Bob is cold.
True
2
proof
[(((triple2) -> rule5))]
("Bob" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "cold" "-")
((triple2) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is big.
True
3
proof
[(((((triple4) -> rule5)) -> rule3))]
("Dave" "is" "big" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule3))]
("Dave" "is" "big" "-")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
True
5
proof
[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule4))]
("Dave" "is" "nice" "+")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule4))]
("Dave" "is" "nice" "-")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1 OR ((((triple2) -> rule5)) -> rule3))] Bob is furry.[(triple2)] Bob is nice.[(triple3 OR ((triple2 triple1) -> rule4) OR ((triple2 ((((triple2) -> rule5)) -> rule3)) -> rule4))] Dave is furry.[(triple4)] Dave is red.[(triple5)] Harry is big.[(triple6 OR ((((triple7) -> rule5)) -> rule3))] Harry is furry.[(triple7)] Harry is nice.[(triple8 OR ((triple7 triple6) -> rule4) OR ((triple7 ((((triple7) -> rule5)) -> rule3)) -> rule4))] Harry is red.[(triple9)] Harry is smart.[(triple10 OR ((triple7 triple6) -> rule2) OR ((triple7 ((((triple7) -> rule5)) -> rule3)) -> rule2))] @1: Bob is cold.[(((triple2) -> rule5))] Bob is smart.[(((triple2 triple1) -> rule2) OR ((triple2 ((((triple2) -> rule5)) -> rule3)) -> rule2))] Dave is cold.[(((triple4) -> rule5))] Harry is cold.[(((triple7) -> rule5))] @2: Dave is big.[(((((triple4) -> rule5)) -> rule3))] @3: Dave is nice.[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule4))] Dave is smart.[(((triple4 ((((triple4) -> rule5)) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple2 triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7 triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple7 triple6) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3