Bob is big. Charlie is not furry. Dave is quiet. All cold, big people are round. If someone is cold then they are round. Big people are cold. If Charlie is not round then Charlie is quiet. Round, big people are green. Quiet people are green.
Bob is big.
("Bob" "is" "big" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
All cold, big people are round.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is not round then Charlie is quiet.
((("Charlie" "is" "round" "~")) -> ("Charlie" "is" "quiet" "+"))
Round, big people are green.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Charlie is not furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Dave is green.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "green" "+")
((triple3) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule3) triple1) -> rule1))]
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule3) triple1) -> rule1))]
("Bob" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
True
5
proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule5) OR ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not green.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule5) OR ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "green" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is big.[(triple1)] Charlie is not furry.[(triple2)] Dave is quiet.[(triple3)] @1: Bob is cold.[(((triple1) -> rule3))] Dave is green.[(((triple3) -> rule6))] @2: Bob is round.[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule3) triple1) -> rule1))] @3: Bob is green.[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule5) OR ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3