Bob is young. Charlie is blue. Charlie is cold. Charlie is kind. Charlie is red. Charlie is smart. Charlie is young. Gary is blue. Gary is kind. Gary is red. Gary is smart. Gary is young. If something is young and rough then it is smart. If something is rough and smart then it is red. Kind, young things are rough.
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young and rough then it is smart.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is rough and smart then it is red.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Kind, young things are rough.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Charlie is kind.
True
1
proof
[(triple4)]
("Charlie" "is" "kind" "+")
triple4
Charlie is not red.
False
1
inv-proof
[(triple5 OR ((((triple4 triple7) -> rule3) triple6) -> rule2) OR ((((triple4 triple7) -> rule3) ((triple7 ((triple4 triple7) -> rule3)) -> rule1)) -> rule2))]
("Charlie" "is" "red" "-")
triple5
((((triple4 triple7) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4 triple7) -> (rule3 % int3)) ((triple7 ((triple4 triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is rough.
True
3
proof
[(((triple4 triple7) -> rule3))]
("Charlie" "is" "rough" "+")
((triple4 triple7) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is not rough.
False
3
inv-proof
[(((triple9 triple12) -> rule3))]
("Gary" "is" "rough" "-")
((triple9 triple12) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is young.[(triple1)] Charlie is blue.[(triple2)] Charlie is cold.[(triple3)] Charlie is kind.[(triple4)] Charlie is red.[(triple5 OR ((((triple4 triple7) -> rule3) triple6) -> rule2) OR ((((triple4 triple7) -> rule3) ((triple7 ((triple4 triple7) -> rule3)) -> rule1)) -> rule2))] Charlie is smart.[(triple6 OR ((triple7 ((triple4 triple7) -> rule3)) -> rule1))] Charlie is young.[(triple7)] Gary is blue.[(triple8)] Gary is kind.[(triple9)] Gary is red.[(triple10 OR ((((triple9 triple12) -> rule3) triple11) -> rule2) OR ((((triple9 triple12) -> rule3) ((triple12 ((triple9 triple12) -> rule3)) -> rule1)) -> rule2))] Gary is smart.[(triple11 OR ((triple12 ((triple9 triple12) -> rule3)) -> rule1))] Gary is young.[(triple12)] @1: Charlie is rough.[(((triple4 triple7) -> rule3))] Gary is rough.[(((triple9 triple12) -> rule3))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((((triple4 triple7) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4 triple7) -> (rule3 % int3)) ((triple7 ((triple4 triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple7 ((triple4 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
((((triple9 triple12) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple9 triple12) -> (rule3 % int3)) ((triple12 ((triple9 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple11
((triple12 ((triple9 triple12) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4 triple7) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple9 triple12) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1