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