Anne is big. Bob is big. Charlie is smart. Fiona is quiet. If Fiona is red then Fiona is rough. Big, red things are rough. All green things are red. All quiet things are green. If something is quiet and not furry then it is green. If something is green then it is quiet.
Anne is big.
("Anne" "is" "big" "+")
Bob is big.
("Bob" "is" "big" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If Fiona is red then Fiona is rough.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "rough" "+"))
Big, red things are rough.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is quiet and not furry then it is green.
((("something" "is" "quiet" "+") ("something" "is" "furry" "~")) -> ("something" "is" "green" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Bob is big.
True
1
proof
[(triple2)]
("Bob" "is" "big" "+")
triple2
Bob is not big.
False
1
inv-proof
[(triple2)]
("Bob" "is" "big" "-")
triple2
Fiona is green.
True
2
proof
[(((triple4) -> rule4))]
("Fiona" "is" "green" "+")
((triple4) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple4) -> rule4))]
("Fiona" "is" "green" "-")
((triple4) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("Fiona" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("Fiona" "is" "red" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
True
4
proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule1))]
("Fiona" "is" "rough" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not rough.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule1))]
("Fiona" "is" "rough" "-")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is red.
Unknown
rconc
[@4: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Bob is red.
Unknown
rconc
[@4: Bob is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule6 <- rule5 <- FAIL)]]
("Bob" "is" "red" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is big.[(triple1)] Bob is big.[(triple2)] Charlie is smart.[(triple3)] Fiona is quiet.[(triple4)] @1: Fiona is green.[(((triple4) -> rule4))] @2: Fiona is red.[(((((triple4) -> rule4)) -> rule3))] @3: Fiona is rough.[(((((((triple4) -> rule4)) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
((triple4) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3