Charlie is kind. Charlie is quiet. Charlie is smart. Dave is kind. Dave is quiet. Dave is white. Erin is quiet. Erin is white. Fiona is green. Fiona is smart. Smart, young things are green. If something is quiet and cold then it is kind. If something is young then it is smart. If something is smart then it is cold. If Erin is quiet then Erin is smart. If Charlie is cold then Charlie is young. White, kind things are smart. If something is smart and green then it is cold.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart, young things are green.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is quiet and cold then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Erin is quiet then Erin is smart.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "smart" "+"))
If Charlie is cold then Charlie is young.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "young" "+"))
White, kind things are smart.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is smart and green then it is cold.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Fiona is smart.
True
1
proof
[(triple10)]
("Fiona" "is" "smart" "+")
triple10
Dave is not kind.
False
1
inv-proof
[(triple4)]
("Dave" "is" "kind" "-")
triple4
Erin is smart.
True
2
proof
[(((triple7) -> rule5))]
("Erin" "is" "smart" "+")
((triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is not smart.
False
3
inv-proof
[(((triple6 triple4) -> rule7))]
("Dave" "is" "smart" "-")
((triple6 triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
True
4
proof
[(((((triple6 triple4) -> rule7)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple6 triple4) -> (rule7 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule4))]
("Erin" "is" "cold" "-")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
True
5
proof
[(((triple7 ((((triple7) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "kind" "+")
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Charlie is not green.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule4)) -> rule6)) -> rule1))]
("Charlie" "is" "green" "-")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is kind.[(triple1 OR ((triple2 ((triple3) -> rule4)) -> rule2))] Charlie is quiet.[(triple2)] Charlie is smart.[(triple3)] Dave is kind.[(triple4)] Dave is quiet.[(triple5)] Dave is white.[(triple6)] Erin is quiet.[(triple7)] Erin is white.[(triple8)] Fiona is green.[(triple9)] Fiona is smart.[(triple10)] @1: Charlie is cold.[(((triple3) -> rule4))] Dave is smart.[(((triple6 triple4) -> rule7))] Erin is smart.[(((triple7) -> rule5))] Fiona is cold.[(((triple10) -> rule4) OR ((triple10 triple9) -> rule8))] @2: Charlie is young.[(((((triple3) -> rule4)) -> rule6))] Dave is cold.[(((((triple6 triple4) -> rule7)) -> rule4))] Erin is cold.[(((((triple7) -> rule5)) -> rule4))] @3: Charlie is green.[(((triple3 ((((triple3) -> rule4)) -> rule6)) -> rule1))] Erin is kind.[(((triple7 ((((triple7) -> rule5)) -> rule4)) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
((triple2 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple6 triple4) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple10 triple9) -> (rule8 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple6 triple4) -> (rule7 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((triple7 ((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3