Anne is big. Bob is not nice. Dave is big. Erin is cold. If something is nice then it is furry. All big things are young. Rough things are young. Cold, red things are rough. If something is young and not big then it is rough. Cold things are rough. All young, nice things are red. Big things are nice.
Anne is big.
("Anne" "is" "big" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Dave is big.
("Dave" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Cold, red things are rough.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is young and not big then it is rough.
((("something" "is" "young" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All young, nice things are red.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Bob is nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Anne is young.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule8))]
("Dave" "is" "nice" "-")
((triple3) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is young.
True
3
proof
[(((((triple4) -> rule6)) -> rule3))]
("Erin" "is" "young" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Dave is not red.
False
5
inv-proof
[(((((triple3) -> rule2) ((triple3) -> rule8)) -> rule7))]
("Dave" "is" "red" "-")
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "red" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is big.[(triple1)] Bob is not nice.[(triple2)] Dave is big.[(triple3)] Erin is cold.[(triple4)] @1: Anne is nice.[(((triple1) -> rule8))] Anne is young.[(((triple1) -> rule2))] Dave is nice.[(((triple3) -> rule8))] Dave is young.[(((triple3) -> rule2))] Erin is rough.[(((triple4) -> rule6))] @2: Anne is furry.[(((((triple1) -> rule8)) -> rule1))] Anne is red.[(((((triple1) -> rule2) ((triple1) -> rule8)) -> rule7))] Dave is furry.[(((((triple3) -> rule8)) -> rule1))] Dave is red.[(((((triple3) -> rule2) ((triple3) -> rule8)) -> rule7))] Erin is young.[(((((triple4) -> rule6)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2