Anne is big. Charlie is big. Fiona is young. Gary is big. Cold things are big. All big things are green. Red things are cold. All red, cold things are quiet. All young, round things are quiet. If something is quiet and young then it is round. If Charlie is green then Charlie is red. All young things are quiet.
Anne is big.
("Anne" "is" "big" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All red, cold things are quiet.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All young, round things are quiet.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and young then it is round.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If Charlie is green then Charlie is red.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "red" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Gary is not big.
False
1
inv-proof
[(triple4)]
("Gary" "is" "big" "-")
triple4
Fiona is quiet.
True
2
proof
[(((triple3) -> rule8))]
("Fiona" "is" "quiet" "+")
((triple3) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "green" "-")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is big.[(triple1)] Charlie is big.[(triple2)] Fiona is young.[(triple3)] Gary is big.[(triple4)] @1: Anne is green.[(((triple1) -> rule2))] Charlie is green.[(((triple2) -> rule2))] Fiona is quiet.[(((triple3) -> rule8))] Gary is green.[(((triple4) -> rule2))] @2: Charlie is red.[(((((triple2) -> rule2)) -> rule7))] Fiona is round.[(((((triple3) -> rule8) triple3) -> rule6))] @3: Charlie is cold.[(((((((triple2) -> rule2)) -> rule7)) -> rule3))] @4: Charlie is quiet.[(((((((triple2) -> rule2)) -> rule7) ((((((triple2) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple4) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple3) -> (rule8 % int2)) triple3) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule2 % int4))) -> (rule7 % int3)) ((((((triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4