Erin is cold. Fiona is big. Gary is smart. Harry is smart. If Fiona is big then Fiona is blue. All blue, big things are round. Blue things are young. All cold, white things are young. If something is cold then it is big. If Fiona is young and Fiona is blue then Fiona is cold. All smart things are white. If something is smart and white then it is round.
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Fiona is big then Fiona is blue.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "blue" "+"))
All blue, big things are round.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All cold, white things are young.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Fiona is young and Fiona is blue then Fiona is cold.
((("Fiona" "is" "young" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "cold" "+"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is smart and white then it is round.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Erin is cold.
True
1
proof
[(triple1)]
("Erin" "is" "cold" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Gary is white.
True
2
proof
[(((triple3) -> rule7))]
("Gary" "is" "white" "+")
((triple3) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "white" "-")
((triple4) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Fiona is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Fiona" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not round.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Fiona" "is" "round" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is cold.
True
6
proof
[(((((((triple2) -> rule1)) -> rule3) ((triple2) -> rule1)) -> rule6))]
("Fiona" "is" "cold" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is not cold.
False
6
inv-proof
[(((((((triple2) -> rule1)) -> rule3) ((triple2) -> rule1)) -> rule6))]
("Fiona" "is" "cold" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "white" "+")
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "young" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Erin is cold.[(triple1)] Fiona is big.[(triple2)] Gary is smart.[(triple3)] Harry is smart.[(triple4)] @1: Erin is big.[(((triple1) -> rule5))] Fiona is blue.[(((triple2) -> rule1))] Gary is white.[(((triple3) -> rule7))] Harry is white.[(((triple4) -> rule7))] @2: Fiona is round.[(((((triple2) -> rule1) triple2) -> rule2))] Fiona is young.[(((((triple2) -> rule1)) -> rule3))] Gary is round.[(((triple3 ((triple3) -> rule7)) -> rule8))] Harry is round.[(((triple4 ((triple4) -> rule7)) -> rule8))] @3: Fiona is cold.[(((((((triple2) -> rule1)) -> rule3) ((triple2) -> rule1)) -> rule6))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple4 ((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3