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