Bob is big. Bob is furry. Bob is red. Bob is rough. Erin is cold. Erin is red. Fiona is red. Harry is blue. Harry is cold. Harry is red. All red, rough people are blue. Blue people are cold. If someone is red and cold then they are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
All red, rough people are blue.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is red and cold then they are young.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple10)]
("Harry" "is" "red" "-")
triple10
Bob is blue.
True
3
proof
[(((triple3 triple4) -> rule1))]
("Bob" "is" "blue" "+")
((triple3 triple4) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is not young.
False
3
inv-proof
[(((triple6 triple5) -> rule3))]
("Erin" "is" "young" "-")
((triple6 triple5) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is cold.
True
4
proof
[(((((triple3 triple4) -> rule1)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple3 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((((triple3 triple4) -> rule1)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple3 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
True
6
proof
[(((triple3 ((((triple3 triple4) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "young" "+")
((triple3 ((((triple3 triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not young.
False
6
inv-proof
[(((triple3 ((((triple3 triple4) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "young" "-")
((triple3 ((((triple3 triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is young.
Unknown
rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is red.[(triple3)] Bob is rough.[(triple4)] Erin is cold.[(triple5)] Erin is red.[(triple6)] Fiona is red.[(triple7)] Harry is blue.[(triple8)] Harry is cold.[(triple9 OR ((triple8) -> rule2))] Harry is red.[(triple10)] @1: Bob is blue.[(((triple3 triple4) -> rule1))] Erin is young.[(((triple6 triple5) -> rule3))] Harry is young.[(((triple10 triple9) -> rule3) OR ((triple10 ((triple8) -> rule2)) -> rule3))] @2: Bob is cold.[(((((triple3 triple4) -> rule1)) -> rule2))] @3: Bob is young.[(((triple3 ((((triple3 triple4) -> rule1)) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 triple4) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple6 triple5) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10 triple9) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple3 triple4) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple3 ((((triple3 triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3