Bob is cold. Bob is kind. Bob is quiet. Bob is red. Dave is quiet. Erin is big. Erin is furry. Erin is kind. Erin is quiet. Fiona is furry. All quiet, big people are rough. If someone is quiet and red then they are cold. All quiet people are kind. If Bob is quiet then Bob is big. If someone is big then they are furry. All quiet, big people are red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All quiet, big people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and red then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Bob is quiet then Bob is big.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "big" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All quiet, big people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Bob is quiet.
True
1
proof
[(triple3)]
("Bob" "is" "quiet" "+")
triple3
Bob is not red.
False
1
inv-proof
[(triple4 OR ((triple3 ((triple3) -> rule4)) -> rule6))]
("Bob" "is" "red" "-")
triple4
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is big.
True
2
proof
[(((triple3) -> rule4))]
("Bob" "is" "big" "+")
((triple3) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Erin is not rough.
False
3
inv-proof
[(((triple9 triple6) -> rule1))]
("Erin" "is" "rough" "-")
((triple9 triple6) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is rough.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule1))]
("Bob" "is" "rough" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("Bob" "is" "furry" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "cold" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is cold.[(triple1 OR ((triple3 triple4) -> rule2) OR ((triple3 ((triple3 ((triple3) -> rule4)) -> rule6)) -> rule2))] Bob is kind.[(triple2 OR ((triple3) -> rule3))] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple3 ((triple3) -> rule4)) -> rule6))] Dave is quiet.[(triple5)] Erin is big.[(triple6)] Erin is furry.[(triple7 OR ((triple6) -> rule5))] Erin is kind.[(triple8 OR ((triple9) -> rule3))] Erin is quiet.[(triple9)] Fiona is furry.[(triple10)] @1: Bob is big.[(((triple3) -> rule4))] Dave is kind.[(((triple5) -> rule3))] Erin is red.[(((triple9 triple6) -> rule6))] Erin is rough.[(((triple9 triple6) -> rule1))] @2: Bob is furry.[(((((triple3) -> rule4)) -> rule5))] Bob is rough.[(((triple3 ((triple3) -> rule4)) -> rule1))] Erin is cold.[(((triple9 ((triple9 triple6) -> rule6)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple3 triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 ((triple3 ((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple3 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple6) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple9) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Bob is big.
("Bob" "is" "big" "+")
((triple3) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple9 triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple9 triple6) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple9 ((triple9 triple6) -> (rule6 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2