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