Bob is white. Charlie is quiet. Fiona is young. Gary is smart. All white people are smart. If Fiona is cold then Fiona is red. All smart people are young. Smart, young people are red. If Charlie is smart then Charlie is white. Smart people are young.
Bob is white.
("Bob" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is cold then Fiona is red.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "red" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Smart, young people are red.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Charlie is smart then Charlie is white.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "white" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Gary is young.
True
2
proof
[(((triple4) -> rule3) OR ((triple4) -> rule6))]
("Gary" "is" "young" "+")
((triple4) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple4) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple4) -> rule6))]
("Gary" "is" "young" "-")
((triple4) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple4) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
True
4
proof
[(((triple4 ((triple4) -> rule3)) -> rule4) OR ((triple4 ((triple4) -> rule6)) -> rule4))]
("Gary" "is" "red" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule6))]
("Bob" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is red.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule4))]
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not red.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule4))]
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is white.[(triple1)] Charlie is quiet.[(triple2)] Fiona is young.[(triple3)] Gary is smart.[(triple4)] @1: Bob is smart.[(((triple1) -> rule1))] Gary is young.[(((triple4) -> rule3) OR ((triple4) -> rule6))] @2: Bob is young.[(((((triple1) -> rule1)) -> rule3) OR ((((triple1) -> rule1)) -> rule6))] Gary is red.[(((triple4 ((triple4) -> rule3)) -> rule4) OR ((triple4 ((triple4) -> rule6)) -> rule4))] @3: Bob is red.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule4) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule4))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple4) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple4) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3