Bob is big. Bob is blue. Bob is cold. Bob is green. Bob is not kind. Bob is not rough. Bob is young. Charlie is cold. Charlie is rough. Charlie is young. Dave is kind. Dave is young. Erin is big. Erin is not cold. Erin is not green. Erin is not rough. If something is big and rough then it is green. If something is kind then it is blue. If something is blue then it is big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not green.
("Erin" "is" "green" "-")
Erin is not rough.
("Erin" "is" "rough" "-")
If something is big and rough then it is green.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Charlie is cold.
True
1
proof
[(triple8)]
("Charlie" "is" "cold" "+")
triple8
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule3))]
("Bob" "is" "big" "-")
triple1
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is blue.
True
2
proof
[(((triple11) -> rule2))]
("Dave" "is" "blue" "+")
((triple11) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple11) -> rule2))]
("Dave" "is" "blue" "-")
((triple11) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
True
3
proof
[(((((triple11) -> rule2)) -> rule3))]
("Dave" "is" "big" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule3))]
("Dave" "is" "big" "-")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is green.
Unknown
rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule3))] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is green.[(triple4)] Bob is not kind.[(triple5)] Bob is not rough.[(triple6)] Bob is young.[(triple7)] Charlie is cold.[(triple8)] Charlie is rough.[(triple9)] Charlie is young.[(triple10)] Dave is kind.[(triple11)] Dave is young.[(triple12)] Erin is big.[(triple13)] Erin is not cold.[(triple14)] Erin is not green.[(triple15)] Erin is not rough.[(triple16)] @1: Dave is blue.[(((triple11) -> rule2))] @2: Dave is big.[(((((triple11) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is not kind.
("Bob" "is" "kind" "-")
triple5
Bob is not rough.
("Bob" "is" "rough" "-")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Erin is big.
("Erin" "is" "big" "+")
triple13
Erin is not cold.
("Erin" "is" "cold" "-")
triple14
Erin is not green.
("Erin" "is" "green" "-")
triple15
Erin is not rough.
("Erin" "is" "rough" "-")
triple16
Dave is blue.
("Dave" "is" "blue" "+")
((triple11) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2