Bob is round. Bob is young. Charlie is cold. Charlie is smart. Charlie is young. Fiona is cold. Gary is young. If someone is nice and white then they are smart. All young people are smart. All nice people are cold. Green, smart people are cold. If Gary is smart then Gary is green. Nice, green people are white. If Charlie is young then Charlie is nice. If someone is cold then they are young. All smart, cold people are nice.
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is nice and white then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Green, smart people are cold.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Gary is smart then Gary is green.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "green" "+"))
Nice, green people are white.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Charlie is young then Charlie is nice.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "nice" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All smart, cold people are nice.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Fiona is cold.
True
1
proof
[(triple6)]
("Fiona" "is" "cold" "+")
triple6
Charlie is not young.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule8))]
("Charlie" "is" "young" "-")
triple5
((triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is smart.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is green.
True
3
proof
[(((((triple7) -> rule2)) -> rule5))]
("Gary" "is" "green" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule5))]
("Gary" "is" "green" "-")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Fiona is nice.
True
5
proof
[(((((((triple6) -> rule8)) -> rule2) triple6) -> rule9))]
("Fiona" "is" "nice" "+")
((((((triple6) -> (rule8 % int3))) -> (rule2 % int2)) triple6) -> (rule9 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not nice.
False
5
inv-proof
[(((((((triple6) -> rule8)) -> rule2) triple6) -> rule9))]
("Fiona" "is" "nice" "-")
((((((triple6) -> (rule8 % int3))) -> (rule2 % int2)) triple6) -> (rule9 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Gary is nice.
True
9
proof
[(((((triple7) -> rule2) ((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4)) -> rule9))]
("Gary" "is" "nice" "+")
((((triple7) -> (rule2 % int4)) ((((((triple7) -> (rule2 % int4))) -> (rule5 % int3)) ((triple7) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule9 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not nice.
False
9
inv-proof
[(((((triple7) -> rule2) ((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4)) -> rule9))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule2 % int4)) ((((((triple7) -> (rule2 % int4))) -> (rule5 % int3)) ((triple7) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule9 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is white.
True
13
proof
[(((((((triple7) -> rule2) ((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4)) -> rule9) ((((triple7) -> rule2)) -> rule5)) -> rule6))]
("Gary" "is" "white" "+")
((((((triple7) -> (rule2 % int5)) ((((((triple7) -> (rule2 % int5))) -> (rule5 % int4)) ((triple7) -> (rule2 % int5))) -> (rule4 % int3))) -> (rule9 % int2)) ((((triple7) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is not white.
False
13
inv-proof
[(((((((triple7) -> rule2) ((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4)) -> rule9) ((((triple7) -> rule2)) -> rule5)) -> rule6))]
("Gary" "is" "white" "-")
((((((triple7) -> (rule2 % int5)) ((((((triple7) -> (rule2 % int5))) -> (rule5 % int4)) ((triple7) -> (rule2 % int5))) -> (rule4 % int3))) -> (rule9 % int2)) ((((triple7) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "+")
Bob is not cold.
Unknown
inv-rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule9 <- rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not nice.
Unknown
inv-rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule9 <- rule3 <- FAIL)]]
("Bob" "is" "nice" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Bob is round.[(triple1)] Bob is young.[(triple2)] Charlie is cold.[(triple3 OR ((((triple5) -> rule7)) -> rule3))] Charlie is smart.[(triple4 OR ((triple5) -> rule2) OR ((((triple3) -> rule8)) -> rule2))] Charlie is young.[(triple5 OR ((triple3) -> rule8))] Fiona is cold.[(triple6)] Gary is young.[(triple7)] @1: Bob is smart.[(((triple2) -> rule2))] Charlie is nice.[(((triple5) -> rule7) OR ((triple4 triple3) -> rule9) OR ((((triple3) -> rule8)) -> rule7) OR ((((triple5) -> rule2) triple3) -> rule9) OR ((((((triple3) -> rule8)) -> rule2) triple3) -> rule9))] Fiona is young.[(((triple6) -> rule8))] Gary is smart.[(((triple7) -> rule2))] @2: Fiona is smart.[(((((triple6) -> rule8)) -> rule2))] Gary is green.[(((((triple7) -> rule2)) -> rule5))] @3: Fiona is nice.[(((((((triple6) -> rule8)) -> rule2) triple6) -> rule9))] Gary is cold.[(((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4))] @4: Gary is nice.[(((((triple7) -> rule2) ((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4)) -> rule9))] @5: Gary is white.[(((((((triple7) -> rule2) ((((((triple7) -> rule2)) -> rule5) ((triple7) -> rule2)) -> rule4)) -> rule9) ((((triple7) -> rule2)) -> rule5)) -> rule6))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple5) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple4 triple3) -> (rule9 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple5) -> (rule2 % int2)) triple3) -> (rule9 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((((triple3) -> (rule8 % int3))) -> (rule2 % int2)) triple3) -> (rule9 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple6) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((triple6) -> (rule8 % int3))) -> (rule2 % int2)) triple6) -> (rule9 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple7) -> (rule2 % int3))) -> (rule5 % int2)) ((triple7) -> (rule2 % int3))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((triple7) -> (rule2 % int4)) ((((((triple7) -> (rule2 % int4))) -> (rule5 % int3)) ((triple7) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule9 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((((((triple7) -> (rule2 % int5)) ((((((triple7) -> (rule2 % int5))) -> (rule5 % int4)) ((triple7) -> (rule2 % int5))) -> (rule4 % int3))) -> (rule9 % int2)) ((((triple7) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5