Anne is cold. Anne is furry. Anne is red. Anne is rough. Charlie is furry. Charlie is not kind. Charlie is rough. Erin is furry. Erin is kind. Erin is nice. Harry is young. All rough things are nice. Young things are kind. If Harry is kind then Harry is rough. If something is red and rough then it is cold. If something is nice then it is cold. If something is nice and cold then it is red. All nice things are furry.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If Harry is kind then Harry is rough.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "rough" "+"))
If something is red and rough then it is cold.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice and cold then it is red.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Anne is red.
True
1
proof
[(triple3 OR ((((triple4) -> rule1) triple1) -> rule6) OR ((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule5)) -> rule6))]
("Anne" "is" "red" "+")
triple3
((((triple4) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Erin is not nice.
False
1
inv-proof
[(triple10)]
("Erin" "is" "nice" "-")
triple10
Erin is cold.
True
2
proof
[(((triple10) -> rule5))]
("Erin" "is" "cold" "+")
((triple10) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple10) -> rule5))]
("Erin" "is" "cold" "-")
((triple10) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple7) -> rule1)) -> rule5))]
("Charlie" "is" "cold" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule3))]
("Harry" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
True
4
proof
[(((((((triple11) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "nice" "+")
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple11) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "nice" "-")
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
True
5
proof
[(((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "furry" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is not furry.
False
5
inv-proof
[(((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "furry" "-")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is red.
True
10
proof
[(((((((((triple11) -> rule2)) -> rule3)) -> rule1) ((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "red" "+")
((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) ((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5
Harry is not red.
False
10
inv-proof
[(((((((((triple11) -> rule2)) -> rule3)) -> rule1) ((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "red" "-")
((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) ((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Anne is cold.[(triple1 OR ((triple3 triple4) -> rule4) OR ((((triple4) -> rule1)) -> rule5))] Anne is furry.[(triple2 OR ((((triple4) -> rule1)) -> rule7))] Anne is red.[(triple3 OR ((((triple4) -> rule1) triple1) -> rule6) OR ((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule5)) -> rule6))] Anne is rough.[(triple4)] Charlie is furry.[(triple5 OR ((((triple7) -> rule1)) -> rule7))] Charlie is not kind.[(triple6)] Charlie is rough.[(triple7)] Erin is furry.[(triple8 OR ((triple10) -> rule7))] Erin is kind.[(triple9)] Erin is nice.[(triple10)] Harry is young.[(triple11)] @1: Anne is nice.[(((triple4) -> rule1))] Charlie is nice.[(((triple7) -> rule1))] Erin is cold.[(((triple10) -> rule5))] Harry is kind.[(((triple11) -> rule2))] @2: Charlie is cold.[(((((triple7) -> rule1)) -> rule5))] Erin is red.[(((triple10 ((triple10) -> rule5)) -> rule6))] Harry is rough.[(((((triple11) -> rule2)) -> rule3))] @3: Charlie is red.[(((((triple7) -> rule1) ((((triple7) -> rule1)) -> rule5)) -> rule6))] Harry is nice.[(((((((triple11) -> rule2)) -> rule3)) -> rule1))] @4: Harry is cold.[(((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule5))] Harry is furry.[(((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule7))] @5: Harry is red.[(((((((((triple11) -> rule2)) -> rule3)) -> rule1) ((((((((triple11) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple3 triple4) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple3
((((triple4) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
((triple10) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Harry is young.
("Harry" "is" "young" "+")
triple11
Anne is nice.
("Anne" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple10) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple11) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple10 ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple7) -> (rule1 % int3)) ((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3)) ((((((((triple11) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5