Anne is cold. Anne is green. Fiona is smart. Gary is cold. Gary is green. Gary is round. Gary is smart. Harry is cold. Harry is green. Harry is smart. If Fiona is quiet and Fiona is nice then Fiona is young. All nice, round things are quiet. All quiet, green things are nice. All young, smart things are cold. Round things are green. All smart things are round. If something is cold then it is nice. If Fiona is green then Fiona is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Fiona is quiet and Fiona is nice then Fiona is young.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "young" "+"))
All nice, round things are quiet.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All quiet, green things are nice.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All young, smart things are cold.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Fiona is green then Fiona is cold.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "cold" "+"))
Gary is green.
True
1
proof
[(triple5 OR ((triple6) -> rule5) OR ((((triple7) -> rule6)) -> rule5))]
("Gary" "is" "green" "+")
triple5
((triple6) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Harry is not cold.
False
1
inv-proof
[(triple8)]
("Harry" "is" "cold" "-")
triple8
Harry is round.
True
2
proof
[(((triple10) -> rule6))]
("Harry" "is" "round" "+")
((triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "nice" "-")
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is quiet.
True
5
proof
[(((((triple8) -> rule7) ((triple10) -> rule6)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple8) -> (rule7 % int3)) ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Fiona is not green.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("Fiona" "is" "green" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
True
4
proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule8))]
("Fiona" "is" "cold" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not cold.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule8))]
("Fiona" "is" "cold" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is nice.
True
5
proof
[(((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7))]
("Fiona" "is" "nice" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is not nice.
False
5
inv-proof
[(((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7))]
("Fiona" "is" "nice" "-")
((((((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is quiet.
True
8
proof
[(((((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7) ((triple3) -> rule6)) -> rule2))]
("Fiona" "is" "quiet" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) ((triple3) -> (rule6 % int5))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
Fiona is not quiet.
False
8
inv-proof
[(((((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7) ((triple3) -> rule6)) -> rule2))]
("Fiona" "is" "quiet" "-")
((((((((((triple3) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) ((triple3) -> (rule6 % int5))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "round" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Fiona is smart.[(triple3)] Gary is cold.[(triple4)] Gary is green.[(triple5 OR ((triple6) -> rule5) OR ((((triple7) -> rule6)) -> rule5))] Gary is round.[(triple6 OR ((triple7) -> rule6))] Gary is smart.[(triple7)] Harry is cold.[(triple8)] Harry is green.[(triple9 OR ((((triple10) -> rule6)) -> rule5))] Harry is smart.[(triple10)] @1: Anne is nice.[(((triple1) -> rule7))] Fiona is round.[(((triple3) -> rule6))] Gary is nice.[(((triple4) -> rule7))] Harry is nice.[(((triple8) -> rule7))] Harry is round.[(((triple10) -> rule6))] @2: Fiona is green.[(((((triple3) -> rule6)) -> rule5))] Gary is quiet.[(((((triple4) -> rule7) triple6) -> rule2) OR ((((triple4) -> rule7) ((triple7) -> rule6)) -> rule2))] Harry is quiet.[(((((triple8) -> rule7) ((triple10) -> rule6)) -> rule2))] @3: Fiona is cold.[(((((((triple3) -> rule6)) -> rule5)) -> rule8))] @4: Fiona is nice.[(((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7))] @5: Fiona is quiet.[(((((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7) ((triple3) -> rule6)) -> rule2))] @6: Fiona is young.[(((((((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7) ((triple3) -> rule6)) -> rule2) ((((((((triple3) -> rule6)) -> rule5)) -> rule8)) -> rule7)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
((triple6) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple7) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple8) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple10) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule7 % int2)) triple6) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple8) -> (rule7 % int3)) ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) ((triple3) -> (rule6 % int5))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
int5
Fiona is young.
("Fiona" "is" "young" "+")
((((((((((((triple3) -> (rule6 % int6))) -> (rule5 % int5))) -> (rule8 % int4))) -> (rule7 % int3)) ((triple3) -> (rule6 % int6))) -> (rule2 % int2)) ((((((((triple3) -> (rule6 % int6))) -> (rule5 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
int5
Fiona is round.
("Fiona" "is" "round" "+")
int6