Bob is big. Bob is cold. Dave is cold. Dave is furry. Dave is quiet. Dave is white. Erin is cold. Erin is white. Gary is furry. Gary is white. Furry, big people are smart. All white people are cold. All cold, white people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is white.
("Gary" "is" "white" "+")
Furry, big people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All cold, white people are big.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Gary is furry.
True
1
proof
[(triple9)]
("Gary" "is" "furry" "+")
triple9
Dave is not cold.
False
1
inv-proof
[(triple3 OR ((triple6) -> rule2))]
("Dave" "is" "cold" "-")
triple3
((triple6) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Erin is big.
True
3
proof
[(((triple7 triple8) -> rule3) OR ((((triple8) -> rule2) triple8) -> rule3))]
("Erin" "is" "big" "+")
((triple7 triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not big.
False
3
inv-proof
[(((triple7 triple8) -> rule3) OR ((((triple8) -> rule2) triple8) -> rule3))]
("Erin" "is" "big" "-")
((triple7 triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is big.
True
4
proof
[(((((triple10) -> rule2) triple10) -> rule3))]
("Gary" "is" "big" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Dave is not smart.
False
5
inv-proof
[(((triple4 ((triple3 triple6) -> rule3)) -> rule1) OR ((triple4 ((((triple6) -> rule2) triple6) -> rule3)) -> rule1))]
("Dave" "is" "smart" "-")
((triple4 ((triple3 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple4 ((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Gary is smart.
True
6
proof
[(((triple9 ((((triple10) -> rule2) triple10) -> rule3)) -> rule1))]
("Gary" "is" "smart" "+")
((triple9 ((((triple10) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not smart.
False
6
inv-proof
[(((triple9 ((((triple10) -> rule2) triple10) -> rule3)) -> rule1))]
("Gary" "is" "smart" "-")
((triple9 ((((triple10) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Dave is cold.[(triple3 OR ((triple6) -> rule2))] Dave is furry.[(triple4)] Dave is quiet.[(triple5)] Dave is white.[(triple6)] Erin is cold.[(triple7 OR ((triple8) -> rule2))] Erin is white.[(triple8)] Gary is furry.[(triple9)] Gary is white.[(triple10)] @1: Dave is big.[(((triple3 triple6) -> rule3) OR ((((triple6) -> rule2) triple6) -> rule3))] Erin is big.[(((triple7 triple8) -> rule3) OR ((((triple8) -> rule2) triple8) -> rule3))] Gary is cold.[(((triple10) -> rule2))] @2: Dave is smart.[(((triple4 ((triple3 triple6) -> rule3)) -> rule1) OR ((triple4 ((((triple6) -> rule2) triple6) -> rule3)) -> rule1))] Gary is big.[(((((triple10) -> rule2) triple10) -> rule3))] @3: Gary is smart.[(((triple9 ((((triple10) -> rule2) triple10) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple6) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
((triple3 triple6) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple7 triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple8) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4 ((triple3 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple4 ((((triple6) -> (rule2 % int3)) triple6) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple9 ((((triple10) -> (rule2 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3