Anne is young. Bob is young. Charlie is nice. Gary is young. Nice people are cold. Rough, big people are young. If someone is cold and nice then they are smart. All white people are young. All smart people are rough. All big, white people are smart.
Anne is young.
("Anne" "is" "young" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Rough, big people are young.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and nice then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All white people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All big, white people are smart.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Charlie is cold.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not smart.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule3))]
("Charlie" "is" "smart" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
True
5
proof
[(((((((triple3) -> rule1) triple3) -> rule3)) -> rule5))]
("Charlie" "is" "rough" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not rough.
False
5
inv-proof
[(((((((triple3) -> rule1) triple3) -> rule3)) -> rule5))]
("Charlie" "is" "rough" "-")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is young.[(triple1)] Bob is young.[(triple2)] Charlie is nice.[(triple3)] Gary is young.[(triple4)] @1: Charlie is cold.[(((triple3) -> rule1))] @2: Charlie is smart.[(((((triple3) -> rule1) triple3) -> rule3))] @3: Charlie is rough.[(((((((triple3) -> rule1) triple3) -> rule3)) -> rule5))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3