Bob is big. Dave is young. Erin is rough. If Bob is cold and Bob is blue then Bob is rough. All kind, blue people are rough. If Erin is rough and Erin is cold then Erin is furry. If someone is young and rough then they are big. If someone is rough then they are young. If Erin is big and Erin is young then Erin is cold.
Bob is big.
("Bob" "is" "big" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If Bob is cold and Bob is blue then Bob is rough.
((("Bob" "is" "cold" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "rough" "+"))
All kind, blue people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Erin is rough and Erin is cold then Erin is furry.
((("Erin" "is" "rough" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
If someone is young and rough then they are big.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Erin is big and Erin is young then Erin is cold.
((("Erin" "is" "big" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "cold" "+"))
Dave is young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple2)]
("Dave" "is" "young" "-")
triple2
Erin is young.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "young" "+")
((triple3) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "young" "-")
((triple3) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
True
4
proof
[(((((triple3) -> rule5) triple3) -> rule4))]
("Erin" "is" "big" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not big.
False
4
inv-proof
[(((((triple3) -> rule5) triple3) -> rule4))]
("Erin" "is" "big" "-")
((((triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
True
7
proof
[(((((((triple3) -> rule5) triple3) -> rule4) ((triple3) -> rule5)) -> rule6))]
("Erin" "is" "cold" "+")
((((((triple3) -> (rule5 % int3)) triple3) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not cold.
False
7
inv-proof
[(((((((triple3) -> rule5) triple3) -> rule4) ((triple3) -> rule5)) -> rule6))]
("Erin" "is" "cold" "-")
((((((triple3) -> (rule5 % int3)) triple3) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is big.[(triple1)] Dave is young.[(triple2)] Erin is rough.[(triple3)] @1: Erin is young.[(((triple3) -> rule5))] @2: Erin is big.[(((((triple3) -> rule5) triple3) -> rule4))] @3: Erin is cold.[(((((((triple3) -> rule5) triple3) -> rule4) ((triple3) -> rule5)) -> rule6))] @4: Erin is furry.[(((triple3 ((((((triple3) -> rule5) triple3) -> rule4) ((triple3) -> rule5)) -> rule6)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple3) -> (rule5 % int3)) triple3) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((triple3 ((((((triple3) -> (rule5 % int4)) triple3) -> (rule4 % int3)) ((triple3) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4