Anne is cold. Anne is kind. Anne is smart. Erin is not cold. Erin is green. Erin is kind. Erin is red. Erin is smart. Erin is not white. Fiona is not cold. Fiona is not kind. Harry is white. All red people are kind. All red, cold people are kind. If someone is cold and not smart then they are kind. All rough, cold people are green. If someone is cold and green then they are red. If someone is white then they are cold. If someone is cold then they are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Harry is white.
("Harry" "is" "white" "+")
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All red, cold people are kind.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and not smart then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "kind" "+"))
All rough, cold people are green.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and green then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Fiona is not cold.
True
1
proof
[(triple10)]
("Fiona" "is" "cold" "-")
triple10
Erin is not kind.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule1))]
("Erin" "is" "kind" "-")
triple6
((triple7) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Anne is rough.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple12) -> rule6))]
("Harry" "is" "cold" "-")
((triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is green.
True
4
proof
[(((((triple1) -> rule7) triple1) -> rule4))]
("Anne" "is" "green" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple12) -> rule6)) -> rule7))]
("Harry" "is" "rough" "-")
((((triple12) -> (rule6 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is red.
True
6
proof
[(((triple1 ((((triple1) -> rule7) triple1) -> rule4)) -> rule5))]
("Anne" "is" "red" "+")
((triple1 ((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not red.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule7) triple1) -> rule4)) -> rule5))]
("Anne" "is" "red" "-")
((triple1 ((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Harry is red.
True
9
proof
[(((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5))]
("Harry" "is" "red" "+")
((((triple12) -> (rule6 % int4)) ((((((triple12) -> (rule6 % int4))) -> (rule7 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not red.
False
9
inv-proof
[(((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5))]
("Harry" "is" "red" "-")
((((triple12) -> (rule6 % int4)) ((((((triple12) -> (rule6 % int4))) -> (rule7 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is kind.
True
10
proof
[(((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5)) -> rule1) OR ((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5) ((triple12) -> rule6)) -> rule2))]
("Harry" "is" "kind" "+")
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule7 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule7 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple12) -> (rule6 % int5))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Harry is not kind.
False
10
inv-proof
[(((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5)) -> rule1) OR ((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5) ((triple12) -> rule6)) -> rule2))]
("Harry" "is" "kind" "-")
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule7 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule7 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple12) -> (rule6 % int5))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "rough" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is cold.[(triple1)] Anne is kind.[(triple2 OR ((((triple1 ((((triple1) -> rule7) triple1) -> rule4)) -> rule5)) -> rule1) OR ((((triple1 ((((triple1) -> rule7) triple1) -> rule4)) -> rule5) triple1) -> rule2))] Anne is smart.[(triple3)] Erin is green.[(triple5)] Erin is kind.[(triple6 OR ((triple7) -> rule1))] Erin is not cold.[(triple4)] Erin is not white.[(triple9)] Erin is red.[(triple7)] Erin is smart.[(triple8)] Fiona is not cold.[(triple10)] Fiona is not kind.[(triple11)] Harry is white.[(triple12)] @1: Anne is rough.[(((triple1) -> rule7))] Harry is cold.[(((triple12) -> rule6))] @2: Anne is green.[(((((triple1) -> rule7) triple1) -> rule4))] Harry is rough.[(((((triple12) -> rule6)) -> rule7))] @3: Anne is red.[(((triple1 ((((triple1) -> rule7) triple1) -> rule4)) -> rule5))] Harry is green.[(((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4))] @4: Harry is red.[(((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5))] @5: Harry is kind.[(((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5)) -> rule1) OR ((((((triple12) -> rule6) ((((((triple12) -> rule6)) -> rule7) ((triple12) -> rule6)) -> rule4)) -> rule5) ((triple12) -> rule6)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((triple1 ((((triple1) -> (rule7 % int4)) triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
((((triple1 ((((triple1) -> (rule7 % int4)) triple1) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple7) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
triple4
Erin is not white.
("Erin" "is" "white" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple10
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple12) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple12) -> (rule6 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple12) -> (rule6 % int3))) -> (rule7 % int2)) ((triple12) -> (rule6 % int3))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((triple12) -> (rule6 % int4)) ((((((triple12) -> (rule6 % int4))) -> (rule7 % int3)) ((triple12) -> (rule6 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule7 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((((triple12) -> (rule6 % int5)) ((((((triple12) -> (rule6 % int5))) -> (rule7 % int4)) ((triple12) -> (rule6 % int5))) -> (rule4 % int3))) -> (rule5 % int2)) ((triple12) -> (rule6 % int5))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5