Charlie is furry. Charlie is kind. Fiona is big. Fiona is cold. Fiona is kind. Fiona is rough. Fiona is white. If Charlie is cold then Charlie is big. If Charlie is white and Charlie is kind then Charlie is rough. If something is rough and white then it is big. Quiet, cold things are big. White things are quiet. All furry, kind things are white.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Charlie is cold then Charlie is big.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "big" "+"))
If Charlie is white and Charlie is kind then Charlie is rough.
((("Charlie" "is" "white" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "rough" "+"))
If something is rough and white then it is big.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Quiet, cold things are big.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All furry, kind things are white.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Fiona is rough.
True
1
proof
[(triple6)]
("Fiona" "is" "rough" "+")
triple6
Fiona is not kind.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "kind" "-")
triple5
Charlie is white.
True
3
proof
[(((triple1 triple2) -> rule6))]
("Charlie" "is" "white" "+")
((triple1 triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("Charlie" "is" "white" "-")
((triple1 triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
True
5
proof
[(((((triple1 triple2) -> rule6) triple2) -> rule2))]
("Charlie" "is" "rough" "+")
((((triple1 triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not rough.
False
5
inv-proof
[(((((triple1 triple2) -> rule6) triple2) -> rule2))]
("Charlie" "is" "rough" "-")
((((triple1 triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
True
9
proof
[(((((((triple1 triple2) -> rule6) triple2) -> rule2) ((triple1 triple2) -> rule6)) -> rule3))]
("Charlie" "is" "big" "+")
((((((triple1 triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2)) ((triple1 triple2) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not big.
False
9
inv-proof
[(((((((triple1 triple2) -> rule6) triple2) -> rule2) ((triple1 triple2) -> rule6)) -> rule3))]
("Charlie" "is" "big" "-")
((((((triple1 triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2)) ((triple1 triple2) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is furry.[(triple1)] Charlie is kind.[(triple2)] Fiona is big.[(triple3 OR ((triple6 triple7) -> rule3) OR ((((triple7) -> rule5) triple4) -> rule4))] Fiona is cold.[(triple4)] Fiona is kind.[(triple5)] Fiona is rough.[(triple6)] Fiona is white.[(triple7)] @1: Charlie is white.[(((triple1 triple2) -> rule6))] Fiona is quiet.[(((triple7) -> rule5))] @2: Charlie is quiet.[(((((triple1 triple2) -> rule6)) -> rule5))] Charlie is rough.[(((((triple1 triple2) -> rule6) triple2) -> rule2))] @3: Charlie is big.[(((((((triple1 triple2) -> rule6) triple2) -> rule2) ((triple1 triple2) -> rule6)) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
((triple6 triple7) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple7) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple1 triple2) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1 triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple1 triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2)) ((triple1 triple2) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3